/*
 * TestLorenzo.cpp
 *
 *  Created on: 08/mag/2012
 *      Author: Lorenzo
 */

#include "TestLorenzo.h"

#include "Formula.h"
#include "Clause.h"
#include "Literal.h"
#include "Parser.h"
#include <iostream>
#include "MontecarloSolver.h"
#include "RandomFormulaeGenerator.h"
#include "BackPropagationSolver.h"



void test1()
{
	std::cout<< "----- TEST1 started -----" << std::endl;
	std::cout<< "<formula>: " << "<val>" << " == <expected val>" << std::endl;

	Formula f1;

	/*
	// aggiunge quattro variabili presettate a true
	f1.addVar(true); // <--- 0
	f1.addVar(true); // <--- 1
	f1.addVar(true); // <--- 2
	f1.addVar(true); // <--- 3
	*/

	//aggiunge una clausola
	std::vector<Literal> lits;
	lits.push_back(Literal(0,false,0));
	lits.push_back(Literal(1,false,0));
	lits.push_back(Literal(2,false,0));
	f1.addClause(lits);

	std::cout<< "f1: " << f1.evaluate() << " == 1" << std::endl;

	//aggiunge una clausola
	lits.clear();
	lits.push_back(Literal(0,true,0));
	lits.push_back(Literal(1,false,0));
	lits.push_back(Literal(3,false,0));
	f1.addClause(lits);

	std::cout<< "f1: " << f1.evaluate() << " == 1" << std::endl;

	//aggiunge una clausola
	lits.clear();
	lits.push_back(Literal(0,true,0));
	f1.addClause(lits);

	std::cout<< "f1: " << f1.evaluate() << " == 0" << std::endl;

	// modifica la variabile 0
	f1.setVar(0,false);
	std::cout<< "f1: " << f1.evaluate() << " == 1" << std::endl;


	// crea la formula f2
	Formula f2;

	/*
	// aggiunge tre variabili presettate a false a f2
	f2.addVar(false); // <--- 0
	f2.addVar(false); // <--- 1
	f2.addVar(false); // <--- 2
	*/



	//aggiunge una clausola a f2
	lits.clear();
	lits.push_back(Literal(0,false,0));
	lits.push_back(Literal(1,false,0));
	lits.push_back(Literal(2,false,0));
	f2.addClause(lits);

	f2.setVar(0,false);
	f2.setVar(1,false);
	f2.setVar(2,false);

	std::cout<< "f2: " << f2.evaluate() << " == 0" << std::endl;

	//aggiunge una clausola a f2 e setta var2
	lits.clear();
	lits.push_back(Literal(0,true,0));
	f2.addClause(lits);
	f2.setVar(2,true);

	std::cout<< "f2: " << f2.evaluate() << " == 1" << std::endl;


	Formula f3;

	//f3.addVar(true);

	lits.clear();

	lits.push_back(Literal(0,true,0));

	f3.addClause(lits);

	std::cout<< "f3: " << f3.evaluate() << " == 0" << std::endl;

	std::cout<< "----- TEST1 ended -----" << std::endl;
}

void test2()
{
	std::cout<< std::endl << "----- TEST2 started -----" << std::endl;

	std::vector<Formula*> frms;

	Parser::parseFile("./data/test.txt",frms);

	//frms[3].setVar(0,false);

	for(unsigned int i=0;i<frms.size();i++)
	{
		std::cout << ">" << i << ") " << std::endl;
		std::cout << "val: " << frms[i]->countSatisfiedClauses()<< " su " << frms[i]->countClauses() << std::endl;
		std::cout << "var count: " << frms[i]->varsCount() << std::endl;
	}

	for(unsigned int i=0;i<frms.size();i++)
	{
		delete frms[i];
	}


	std::cout<< "----- TEST2 ended -----" << std::endl;
}


void test3()
{
	std::cout<< std::endl << "----- TEST3 started -----" << std::endl;

	Formula f1;

	std::vector<Literal> lits;
	lits.push_back(Literal(0,false,0));
	lits.push_back(Literal(1,false,0));
	lits.push_back(Literal(2,false,0));
	f1.addClause(lits);

	EvaluationReport er = f1.getEvaluationReport();

	std::cout<< "sat " << er.getsatisfiedClauses() << " on " << er.getClausesNumber() << endl;

	std::cout<< "----- TEST3 ended -----" << std::endl;
}

void test4()
{
	std::cout<< std::endl << "----- TEST4 started -----" << std::endl;

	Formula f1;

	std::vector<Literal> lits;
	lits.push_back(Literal(0,false,0));
	lits.push_back(Literal(1,false,0));
	lits.push_back(Literal(2,false,0));
	f1.addClause(lits);

	lits.clear();
	lits.push_back(Literal(0,true,0));
	lits.push_back(Literal(1,true,0));
	lits.push_back(Literal(3,true,0));
	f1.addClause(lits);

	double epsilon = 0.3;

	EvaluationReport er = MontecarloSolver::randomSolve(f1,epsilon);

	std::cout<< "sat " << er.getsatisfiedClauses() << " on " << er.getClausesNumber() << ", iteration: " << er.getIteration() << endl;

	std::cout<< "----- TEST4 ended -----" << std::endl;
}

void test5()
{
	std::cout<< std::endl << "----- TEST5 started -----" << std::endl;

	std::vector<Formula*> frms;

	Parser::parseFile("./data/test.txt",frms);

	double epsilon = 0.01;

	EvaluationReport er = MontecarloSolver::randomSolve(*frms[7],epsilon);

	std::cout<< "sat " << er.getsatisfiedClauses() << " on " << er.getClausesNumber() << ", iteration: " << er.getIteration() << endl;

	for(unsigned int i=0;i<frms.size();i++)
	{
		delete frms[i];
	}

	std::cout<< "----- TEST5 ended -----" << std::endl;
}


void test6()
{
	std::cout<< std::endl << "----- TEST6 started -----" << std::endl;


	std::vector<Formula*> frms;

	RandomFormulaeGenerator::generateRandomSetOfFormulae(frms,15,16,20,20);

	for(unsigned int i=0;i<frms.size();i++)
	{
		std::cout << ">" << i << ") " << std::endl;
		std::cout << "val: " << frms[i]->countSatisfiedClauses()<< " su " << frms[i]->countClauses() << std::endl;
		std::cout << "var count: " << frms[i]->varsCount() << std::endl;
	}

	for(unsigned int i=0;i<frms.size();i++)
	{
		delete frms[i];
	}

	std::cout<< "----- TEST6 ended -----" << std::endl;
}


void test7()
{
	std::cout<< std::endl << "----- TEST7 started -----" << std::endl;

	std::vector<Formula*> frms;

	Parser::parseFile("./data/test.txt",frms);

	BackPropagationSolver bps;


	for(unsigned int i=0;i<frms.size();i++)
	{
		EvaluationReport er = bps.solve(*frms[i]);

		std::cout<< "sat " << er.getsatisfiedClauses() << " on " << er.getClausesNumber() << ", iteration: " << er.getIteration() << endl;
	}

	for(unsigned int i=0;i<frms.size();i++)
	{
		delete frms[i];
	}

	std::cout<< "----- TEST7 ended -----" << std::endl;
}


void test8()
{
	std::cout<< std::endl << "----- TEST8 started -----" << std::endl;

	std::vector<Formula*> frms;

	RandomFormulaeGenerator::generateRandomSetOfFormulae(frms,3,3,2000,4);

	BackPropagationSolver bps;


	for(unsigned int i=0;i<frms.size();i++)
	{
		EvaluationReport er = bps.solve(*frms[i]);

		std::cout<< "sat " << er.getsatisfiedClauses() << " on " << er.getClausesNumber() << ", iteration: " << er.getIteration() << endl;
	}

	for(unsigned int i=0;i<frms.size();i++)
	{
		delete frms[i];
	}

	std::cout<< "----- TEST8 ended -----" << std::endl;
}



TestLorenzo::TestLorenzo() {
	// TODO Auto-generated constructor stub

}

TestLorenzo::~TestLorenzo() {
	// TODO Auto-generated destructor stub
}

void TestLorenzo::run()
{
	//test0();
	test1();
	test2();
	test3();
	test4();
	test5();
	test6();
	test7();
	test8();
}



